\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$;${\it da}$), ${\it es}$:ES.
\-\\[0ex]msg{-}spec{-}loc(${\it snd}$;$i$) $\Rightarrow$ update{-}spec{-}decl(${\it upd}$;${\it ds}$) $\Rightarrow$ @$i$[[$A$;${\it snd}$;${\it upd}$]] $\in$ Prop
\end{tabbing}